$\forall$$T_{1}$, $T_{2}$:Type, ${\it as}$:$T_{1}$ List, ${\it bs}$:$T_{2}$ List. $\parallel$${\it as}$$\parallel$ $=$ $\parallel$${\it bs}$$\parallel$ $\in$ $\mathbb{Z}$ $\Rightarrow$ unzip(zip(${\it as}$;${\it bs}$)) $=$ $\langle$${\it as}$$,\,$${\it bs}$$\rangle$